| Definitions |  x:A. B(x), P   Q, t  T, if b then t else f fi , tt, ff,  A,  ,   x. t(x),  , A  B, False, SQType(T), {T},  , State(ds), Top, f(x)?z, x dom(f), deq-member(eq;x;L), reduce(f;k;as), Y, t.1, P & Q, {i..j }, i j < k, a:A fp B(a), (x l), Knd,  x:A. B(x), A c B, (link n from i to j), rcv(l,tg),  b, isrcv(k), destination(l), lnk(k), isl(x), t.2, outl(x),  , Unit, P  Q, x(s), Namer(n;Id_list), (xL.P(x)), P  Q, ma-interface-conds(I;i), fpf-domain(f), es-in-port-conds(A;l;tg), P Q,  , a = b |
| Lemmas | ma-interface-loc wf, lsrc wf, bool wf, eqtt to assert, ma-interface-ds wf, assert-ma-interface-loc, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-empty wf, Id wf, gluable2 wf, gluable wf, ma-interface-normal wf, Namer wf, le wf, append wf, lname wf, ma-interface-tags wf, IdLnk wf, ma-interface wf, member-remove-repeats, Id sq, ma-interface-conds wf3, l member wf, remove-repeats wf, id-deq wf, ma-interface-locs wf, es-in-port-conds wf, mk lnk wf, subtype-fpf2, decl-state wf, top wf, subtype rel product, subtype rel function, subtype rel dep function, fpf-cap wf, subtype rel self, subtype-fpf-cap-top, fpf-empty-sub, eq id wf, assert-eq-id, not functionality wrt iff, triggersGlue wf, fpf-join-list wf, Knd wf, mapl wf, nat wf, length wf1, select wf, fpf-dom wf, ma-interface-conds wf, fpf-trivial-subtype-top, fpf wf, fpf-join-list-dom2, subtype rel list, member-mapl, bool cases, bool sq, member-fpf-domain, ma-interface-dom-hasloc, fpf-single-dom-sq, rcv wf, assert-eq-knd, Knd sq, assert-hasloc, true wf |
(mapl(